\begin{tabbing}
recognizer(${\it es}$;$i$;${\it ds}$;$x$;$k$;$T$;${\it test}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(es{-}dtype(${\it es}$;$i$;$x$;$\mathbb{B}$) \& (es{-}state(${\it es}$;$i$) $\subseteq$r State(${\it ds}$)) \& (es{-}kindtype(${\it es}$;$i$;$k$) $\subseteq$r $T$))\+
\\[0ex]c$\wedge$ \=(alle{-}at(${\it es}$;$i$;$e$.($\uparrow$es{-}after(${\it es}$; $x$; $e$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}le(${\it es}$;${\it e'}$;$e$) \& es{-}kind(${\it es}$; ${\it e'}$) = $k$ $\in$ Knd)
\\[0ex]c$\wedge$ ($\uparrow$(${\it test}$(es{-}state{-}when(${\it es}$;${\it e'}$),es{-}val(${\it es}$; ${\it e'}$)))))))
\-\\[0ex]\& es{-}initially(${\it es}$;$i$;$x$) = ff $\in$ $\mathbb{B}$)
\-\-
\end{tabbing}